Section: New Results

Specification and verification of TLA+ and PLC systems

Formal semantics of PLC programming languages

Participants : Sidi Ould Biha, Litian Xiao, Ming Gu.

We formalized a semantics of the Instruction List (IL) language, one of the five programing languages defined in the IEC 61131-3 standard for PLC programing [23] . This semantics support a significant subset of the IL language that includes on-delay timers. This semantics was used in a join work to with Jan Olaf Blech from Fortiss (Germany) to prove some safety properties for a real industrial example of PLC program [18] .

A second widely used language for programming PLC is the graphical language Ladder Diagrams (LD). We defined a formal semantics of LD in the proof assistant Coq. Based on this semantics and the IL one, we developed a translation function from LD to IL. We also proved a semantic preservation property for this translation function. We have now a certified compilation function from the graphical language LD to IL. This work opens the way for the development of a certified compilation chain for PLC. A journal paper about this work and others aspects of PLC certification is under reviewing.

In [16] , [15] , we study the definition of denotational semantics on PLC program language, which is convenient to PLC programs modeling and model checking. The purpose of the work is the correctness verification on PLC programs by formal methods. Based on the extended $\lambda$-calculus definition, this work has defined the configuration of PLC program architecture, denotational semantics of PLC programs and functions of denotational semantics. It is the basis of model checking and theorem proving.

Formalization and verification of PLCs

Participants : Hai Wan, Litian Xiao, Ming Gu.

PLCs are widely used in embedded systems. Timers play a pivotal role in PLC real-time applications. The formalization of timers is of great importance. In [13] , we present a formalization of PLC timers in the theorem proving system Coq, in which the behaviors of timers are characterized by a set of axioms at an abstract level. The authors discuss how to model timers at a proper and sound abstract level. PLC programs with timers are modeled. As a case study, a quiz machine problem with a timer is investigated. This work demonstrates the complexity of formal timer modeling.

In [25] , we modeled kernel data type and basic statements and and the denotational semantics of PLC program in Coq. It has given the correctness proof of PLC program based on theorem proving, i.e. based on semantics function the relationship of configuration between the before codes execution and the after is proved. The main purpose is to prove whether a PLC program satisfies certain nature within a scan period.

Synthesis of PLC programs

Participants : Rui Wang, Ming Gu.

PLCs are complex cyber-physical systems which are widely used in industry. In [14] , we present a robust approach to design and implement PLC-based embedded systems. Timed automata are used to model the controller and its environment. We validate the design model with resort to model checking techniques. We propose an algorithm to generate PLC code from timed automata and implement this algorithm with a prototype tool. This method can condense the developing process and guarantee the correctness of PLC programs. A case study demonstrates the effectiveness of the method.

Domain-driven probabilistic analysis of PLCs

Participants : Hehua Zhang, Yu Jiang, Ming Gu.

Programmable Logic Controllers are widely used in industry. Reliable PLCs are vital to many critical applications. We present a novel symbolic approach for analysis of PLC systems [27] . The main components of the approach consists of: (1) calculating the uncertainty characterization of the PLC systems, (2) abstracting the PLC system as a Hidden Markov Model, (3) solving the Hidden Markov Model using domain knowledge, (4) integrating the solved Hidden Markov Model and the uncertainty characterization to form an integrated (regular) Markov Model, and (5) harnessing probabilistic model checking to analyze properties on the resultant Markov Model. The framework provides expected performance measures of the PLC systems by automated analytical means without expensive simulations. Case studies on an industrial automated system are performed to demonstrate the effectiveness of our approach.

Edola: a domain modeling and verification language for PLCs

Participants : Hehua Zhang, Ming Gu.

Formal modeling and verification of PLC systems become paramount in engineering applications. The work presents a novel PLC domain-specific modeling language Edola [26] . Important characteristics of PLC embedded systems, such as reactivity, scan cycling, real-time and property patterns, are embodied in the language design. Formal verification methods, such as model checking and automatic theorem proving, are supported in Edola modeling. The TLA+ specification language constitutes an intermediate language layer between Edola and the verification tools, enhancing a large degree of reusability. A prototype IDE for Edola and its seamless integration of a model checker TLC and an automatic theorem prover Spass are implemented. A case study illustrates and validates the applicability of the language.